

abstract sig ServizioBase {}

sig Data {
	giorno,mese,anno: Int
	
}



sig Volo extends ServizioBase {
	dataPartenza: one Data,			//data di atterraggio del volo "all'andata"
	dataRitorno: one Data			//data di decollo del volo "al ritorno"
}

sig Hotel extends ServizioBase {
	dataCheckIn: one Data,
	dataCheckOut: one Data
}

sig Escursione extends ServizioBase {
	dataEscursione: one Data
}

//signature che rappresenta il pacchetto offerto dall'agenzia
sig PacchettoOfferto {
	voloPacchetto:  one Volo,
	hotelPacchetto: one Hotel,
	escursionePacchetto: some Escursione
}


//Inizio - fact pacchetti diversi
fact {
	all p, p':PacchettoOfferto | p != p' and p.voloPacchetto = p'.voloPacchetto and
					p.escursionePacchetto = p'.escursionePacchetto =>	p.hotelPacchetto != p'.hotelPacchetto
}

fact {
	all p, p':PacchettoOfferto | p != p' and p.voloPacchetto = p'.voloPacchetto and
						p.hotelPacchetto = p'.hotelPacchetto =>p.escursionePacchetto = p'.escursionePacchetto 
}

fact {
	all p, p':PacchettoOfferto | p != p' and p.hotelPacchetto = p'.hotelPacchetto and
					p.escursionePacchetto = p'.escursionePacchetto =>p.voloPacchetto != p'.voloPacchetto	
}


//Fine - fact pacchetti diversi


//Fatto che impone la consistenza sulle date delle escursioni
fact{
		all p: PacchettoOfferto | all e: p.escursionePacchetto |

				//condizione sugli anni ( annoPartenza =< annoEscursione =< annoRitorno )
				e.dataEscursione.anno =< p.voloPacchetto.dataRitorno.anno and
					e.dataEscursione.anno >= p.voloPacchetto.dataPartenza.anno and

				//se gli anni sono uguali allora i mesi devono essere corretti
				(  e.dataEscursione.anno = p.voloPacchetto.dataRitorno.anno =>
					e.dataEscursione.mese =< p.voloPacchetto.dataRitorno.mese) and
				(  e.dataEscursione.anno = p.voloPacchetto.dataPartenza.anno =>
					e.dataEscursione.mese >= p.voloPacchetto.dataPartenza.mese) 
				
				and

				//se anno e mese sono uguali
					((  e.dataEscursione.anno = p.voloPacchetto.dataRitorno.anno and
					e.dataEscursione.mese = p.voloPacchetto.dataRitorno.mese) => e.dataEscursione.giorno =< p.voloPacchetto.dataRitorno.giorno
					) and
					((  e.dataEscursione.anno = p.voloPacchetto.dataPartenza.anno and
					e.dataEscursione.mese = p.voloPacchetto.dataPartenza.mese) => e.dataEscursione.giorno >= p.voloPacchetto.dataPartenza.giorno
					)

}



	//Fatto che impone che dataPartenza < dataRitorno
fact {
	all p: PacchettoOfferto | p.voloPacchetto.dataPartenza.anno < p.voloPacchetto.dataRitorno.anno or
 
										((p.voloPacchetto.dataPartenza.anno = p.voloPacchetto.dataRitorno.anno and
											p.voloPacchetto.dataPartenza.mese < p.voloPacchetto.dataRitorno.mese) or


										 (p.voloPacchetto.dataPartenza.anno = p.voloPacchetto.dataRitorno.anno and
											p.voloPacchetto.dataPartenza.mese = p.voloPacchetto.dataRitorno.mese and
											p.voloPacchetto.dataPartenza.giorno < p.voloPacchetto.dataRitorno.giorno)
										)
										and 

										//Condizione che verifica che le date di CHECKIN E CHECKOUT dall'hotel siano uguali rispettivamente alle date di partenza e ritorno
										p.voloPacchetto.dataPartenza = p.hotelPacchetto.dataCheckIn and
										p.hotelPacchetto.dataCheckOut = p.voloPacchetto.dataRitorno
}



//asserzione che verifica che non ci possano essere inconsistenze sulle date delle escursioni

assert dateConsistenza {

				no p: PacchettoOfferto, e: p.escursionePacchetto |

						//Condizione sulla data di Ritorno
					(
							e.dataEscursione.anno > p.voloPacchetto.dataRitorno.anno or
								(e.dataEscursione.anno = p.voloPacchetto.dataRitorno.anno and
									e.dataEscursione.mese > p.voloPacchetto.dataRitorno.mese
								) or
								(e.dataEscursione.anno = p.voloPacchetto.dataRitorno.anno and
									e.dataEscursione.mese = p.voloPacchetto.dataRitorno.mese and
										e.dataEscursione.giorno > p.voloPacchetto.dataRitorno.giorno
								)
					) or 
					
					//Condizione sulla data di Partenza
					(
							e.dataEscursione.anno < p.voloPacchetto.dataPartenza.anno or
								(e.dataEscursione.anno = p.voloPacchetto.dataPartenza.anno and
									e.dataEscursione.mese < p.voloPacchetto.dataPartenza.mese
								) or
								(e.dataEscursione.anno = p.voloPacchetto.dataPartenza.anno and
									e.dataEscursione.mese = p.voloPacchetto.dataPartenza.mese and
										e.dataEscursione.giorno < p.voloPacchetto.dataPartenza.giorno
								)
					)
}




//Asserzione che verifica che due pacchetti siano distinti (non abbiano gli stessi volo, hotel, escursioni)

assert pacchettoNonDuplicato {

	no p, p':PacchettoOfferto | p != p' and p.voloPacchetto = p'.voloPacchetto and
					p.escursionePacchetto = p'.escursionePacchetto and
					p.hotelPacchetto = p'.hotelPacchetto
}





//check pacchettoNonDuplicato
//check dateConsistenza





pred show {} 
run show for 6 but 2 PacchettoOfferto

